Inductive ByteEval (s: State) : ByteExp -> option Byte -> Prop :=
  | byte_eval_lit : forall (b:Byte),
      ByteEval s (byte_exp_num b) (Some b)

  | byte_eval_id : forall (i:Id)(b:Byte),
      s i = Some (byte_val b) -> ByteEval s (byte_exp_id i) (Some b)

  | byte_eval_xor : forall (e1 e2: ByteExp)(b1 b2: Byte),
      ByteEval s e1 (Some b1) -> ByteEval s e2 (Some b2) -> ByteEval s (byte_exp_xor e1 e2) (Some (byte_xor b1 b2))

   | byte_eval_andbb : forall (e1 e2: ByteExp)(b1 b2: Byte),
      ByteEval s e1 (Some b1) -> ByteEval s e2 (Some b2) -> ByteEval s (byte_exp_andbb e1 e2) (Some (byte_and b1 b2))

  | byte_eval_shiftl : forall (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      ByteEval s e (Some b) -> ArithEval s n x -> ByteEval s (byte_exp_shiftl e n) (Some (byte_shl b x))

  | byte_eval_shiftr : forall (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      ByteEval s e (Some b) -> ArithEval s n x -> ByteEval s (byte_exp_shiftr e n) (Some (byte_shr b x))

  | byte_eval_matrix : forall aexp1 aexp2 (m n i j: Integer)(mexp: MatrixExp) (matr: Matrix Byte m n),
      MatrixEval s mexp matr -> ArithEval s aexp1 i -> ArithEval s aexp2 j -> ByteEval s (byte_exp_matrix mexp aexp1 aexp2) (matrix_get i j matr)
.
